feat(formal): real-lift R1 — first real ⟦compile p⟧ = ⟦p⟧ (RealCompile.v)#640
Merged
Conversation
🔍 Hypatia Security ScanFindings: 41 issues detected
View findings[
{
"reason": "Action denoland/setup-deno@v2 needs attention",
"type": "unpinned_action",
"file": "publish-jsr.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in instant-sync.yml",
"type": "secret_action_without_presence_gate",
"file": "instant-sync.yml",
"action": "peter-evans/repository-dispatch",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/packages/affinescript-cli/mod.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (2 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/packages/affine-vscode/mod.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/affinescript-vite/src/affine-plugin-improved.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "expect() in hot path (32 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/wasm_gen.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "expect() in hot path (29 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/affine_gen.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (2 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/affinescript/affinescript/runtime/src/panic.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (1 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/affinescript/affinescript/runtime/src/alloc.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (3 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/affinescript/affinescript/runtime/src/ffi.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
…e.v) Climbs the REAL-LIFT ladder (formal/REAL-LIFT.adoc) from R0 to R1: the first mechanized codegen-preservation theorem on the REAL objects — the actual lib/wasm.ml instruction IR and the real (resolved) lib/ast.ml expression core — retiring the toy K1/K1Let on real objects. RealWasm.v (grown): adds locals (LocalGet/LocalSet) and the comparison ops I32Eq/I32LtS, threading a mutable locals store through wexec. wexec is refactored through a per-instruction step1 so the sequencing lemmas wexec_app/wexec_seq (which the preservation proof composes with) are one line each. wexec_sound is retained for the pure (no_local) fragment. RealCompile.v (new, R1): - source rexpr: the resolved int/bool/let/binary core of lib/ast.ml (de Bruijn LEVELS — name resolution is P-7; bool = 0/1, int = Z); - eval: the reference dynamic semantics (mirrors lib/interp.ml); - compile: lowers let to LocalSet into a pre-sized locals array (slot = binding depth; siblings reuse slots), mirroring lib/codegen.ml; - compile_correct: eval env e = Some v -> wexec (compile |env| e) locals st = Some (locals', v :: st), carrying an env<->locals agreement invariant with fresh-slot allocation and low-slot preservation through the induction; - compile_program_correct: runs a closed program from the zero-initialised array. All axiom-free (Print Assumptions: Closed under the global context). formal/ now 17 files, 29 closure reports. Wired into _CoqProject / justfile / .hypatia-ignore / README.adoc; REAL-LIFT.adoc (R1 landed, R2 next) + PROOF-NEEDS.adoc (K-1 row, section 6 Wave 3) updated. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr
hyperpolymath
force-pushed
the
claude/lucid-cray-4a22dp
branch
from
0f902e0 to
bc3ec78
Compare
🔍 Hypatia Security ScanFindings: 41 issues detected
View findings[
{
"reason": "Action denoland/setup-deno@v2 needs attention",
"type": "unpinned_action",
"file": "publish-jsr.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in instant-sync.yml",
"type": "secret_action_without_presence_gate",
"file": "instant-sync.yml",
"action": "peter-evans/repository-dispatch",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/packages/affinescript-cli/mod.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (2 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/packages/affine-vscode/mod.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/affinescript-vite/src/affine-plugin-improved.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "expect() in hot path (32 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/wasm_gen.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "expect() in hot path (29 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/affine_gen.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (2 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/affinescript/affinescript/runtime/src/panic.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (1 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/affinescript/affinescript/runtime/src/alloc.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (3 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/affinescript/affinescript/runtime/src/ffi.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Climbs the REAL-LIFT ladder (
formal/REAL-LIFT.adoc) from R0 → R1: the first mechanized⟦compile p⟧ = ⟦p⟧on the real objects — the actuallib/wasm.mlinstruction IR and the real (resolved)lib/ast.mlexpression core. This retires the toyK1/K1Leton real objects.RealWasm.v(grown for R1)Adds locals (
LocalGet/LocalSet) and the comparison opsI32Eq/I32LtS, threading a mutable locals store throughwexec.wexecis refactored through a per-instructionstep1, so the sequencing lemmaswexec_app/wexec_seq(which the preservation proof composes with) are one line each.wexec_sound(R0) is retained for the pure (no_local) fragment.RealCompile.v(new, R1)rexpr— the resolved int/bool/let/binary core oflib/ast.ml(de Bruijn levels; name resolution is a separate obligation, P-7; bool ≔ 0/1, int ≔ Z, so one observable);eval— the reference dynamic semantics (mirrorslib/interp.ml);compile— lowerslettoLocalSet dinto a pre-sized locals array (slot = binding depthd; siblings reuse slots), mirroringlib/codegen.ml;compile_correct— the theorem:eval env e = Some v → agree env locals → |env| = d → d + depth e ≤ |locals| → ∃ locals', wexec (compile d e) locals st = Some (locals', v :: st) ∧ |locals'| = |locals| ∧ (∀ i < d, nth_error locals' i = nth_error locals i)carrying an env↔locals agreement invariant with fresh-slot allocation and low-slot preservation through the induction (the genuine compiler-correctness simulation);
compile_program_correct— runs a closed program from the zero-initialised locals array.Concrete end-to-end check (
let x = 2+3 in x*4 ⇒ 20):r1_eval_demo(source) andr1_exec_demo(compilethenwexec⇒[20]).Honest scope
R1 is the int/bool/
let/binop fragment on de Bruijn-resolved source;LocalTee/i64, structured control, memory, floats, calls, and effects are later rungs (REAL-LIFT.adoc§4). R2 (structured control on a fuel-indexedwexec) is next, and is the rung that settles #601 concretely.Verification
All axiom-free — every
Print Assumptionsreports Closed under the global context.formal/now 17 files, 29 closure reports (full dep-order recompile, noAxioms:). Wired into_CoqProject/justfile/.hypatia-ignore;README.adoc,REAL-LIFT.adoc(R1 landed, R2 next), andPROOF-NEEDS.adoc(K-1 row, §1, §6 Wave 3) updated.Follow-on to #638 (R0 + plan, merged).
QTT-dynamic #637 ✅ → F-5 + R0 #638 ✅ → **R1 (this)**.🤖 Generated with Claude Code
https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr
Generated by Claude Code